w:World, i, x:Id, k:Knd. w-machine-independent(w;i;k;x)   

latex

Definitions

w-machine-independent(w;i;k;x), World, w-machine(w;i), vartype(i;x), Msg, w.TA, w.T, w.M, w-automaton(T;TA;M), w-kindtype(TA;M;i), kindcase(k; a.f(a); l,t.g(l;t) ), islocal(k), act(k), lnk(k), tag(k), P  Q, a = b, destination(l), , b, b, Void, outr(x), inl x , False, P & Q, A, , type List, P  Q, True, , , s = t, left + right, Type, Unit, #$n, , x.A(x), Knd, inr x , S  T, x:AB(x), x:A  B(x), f(a), Id, IdLnk, rcv(l,tg), locl(a), x:A. B(x), Msg(M), t  T

Lemmas

locl wf, rcv wf, int inc rationals, unit wf, nat wf, true wf, IdLnk wf, Msg wf, rationals wf, not wf, false wf, assert wf, bnot wf, bool wf, ldst wf, eq id wf, assert-eq-id, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, w-automaton wf, Id wf, Knd wf, world wf